#include "cnf_reader.cuh"

int max_variable = -1;

int header_number_of_clauses;
int header_number_of_variables;

int variable_with_more_occurrences;
int max_occurrence_of_variable;

Lit current_clause_lits[MAX_CLAUSE_SIZE];
int current_clause_size = 0;
bool valid_cnf_file = true;

FormulaData * formula_data;

map<int, int> * occurrences;

void set_header(int variables, int clauses)
{
	header_number_of_variables = variables;
	header_number_of_clauses = clauses;
}

void start_new_clause()
{
	current_clause_size = 0;
}

void add_clause()
{
	formula_data->add_clause(current_clause_lits, current_clause_size);
}

void add_lit(Var v, bool sign)
{
#ifdef USE_ASSERTIONS
	assert(current_clause_size < MAX_CLAUSE_SIZE -1);
#endif
	Lit l = mkLit(v, sign);
	current_clause_lits[current_clause_size] = l;
	current_clause_size++;

	if(v+1 > max_variable)
	{
		max_variable = v+1;
	}
	map<int,int>::iterator it = occurrences->find(v);
	if(it == occurrences->end())
	{
		(*occurrences)[v]=1;
	}
	else
	{
		(*occurrences)[v]=(*occurrences)[v]+1;
	}

	if((*occurrences)[v] > max_occurrence_of_variable)
	{
		max_occurrence_of_variable = (*occurrences)[v];
		variable_with_more_occurrences = v;
	}

}

bool read_cnf(char* file, FormulaData & data)

{
	max_variable = -1;
	variable_with_more_occurrences = -1;
	max_occurrence_of_variable = -1;

	bool exists = set_file(file);

	if(!exists)
	{
		yyerror("Could not find CNF file!");
		return false;
	}
	formula_data = &data;
	occurrences = new map<int, int>();

	yyparse_cnf();

	if(max_variable > header_number_of_variables)
	{
		char warning[1000];
		sprintf(warning, "header claims %d variables, "
				"but highest variable found is %d. Using %d...",
				header_number_of_variables, max_variable, max_variable);
		yywarning(warning);
		data.set_number_of_variables(max_variable);
	}
	else
	{
		//data.set_number_of_variables(header_number_of_variables);
		data.set_number_of_variables(max_variable);
	}


	if(formula_data->get_number_of_clauses() != header_number_of_clauses)
	{
		char warning[1000];
        sprintf(warning, "header claims %d clauses, but found %d clauses. Using %d...",
        		header_number_of_clauses, formula_data->get_number_of_clauses(),
        		formula_data->get_number_of_clauses());
        yywarning(warning);
	}

	formula_data->copy_host_clauses_to_dev();

	formula_data->set_most_common_variable(variable_with_more_occurrences, max_occurrence_of_variable);

	delete(occurrences);

	return valid_cnf_file;

}



int yyerror(char* error)
{
	printf("%s (line %d)\n", error, yyget_lineno());
	valid_cnf_file = false;
}

void yywarning(char* warning)
{

	printf("Warning: %s\n", warning);
}

